COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002		Juan Bulnes has just completed his PhD dissertation entitled
C00004 ENDMK
C⊗;
	Juan Bulnes has just completed his PhD dissertation entitled
"GOAL: A Goal Command Language for Interactive Proof Construction."
It is the first goal-directed system for theorem proving in first order
logic built on the basis of a natural deduction proof-checker.
It demonstrates his understanding of mathematical logic and other mathematics,
his ability to program large systems, an excellent understanding
of how to make programs interface with their users, a high degree
of originality and the ability to work independently.  While not the
final word in goal directed interactive theorem proving, his thesis
provides a substantial basis for future work in the area.  His written
and oral presentations of his results were excellent.  Besides this
Bulnes is pleasant and co-operative.